PRISM

Benchmark
Model:majority v.1 (CTMC)
Parameter(s)T = 2100
Property:change_state (prob-reach-time-bounded)
Invocation (default)
./fix-syntax ./prism -javamaxmem 11g -cuddmaxmem 4g  -heuristic speed -ddextraactionvars 100 -maxiters 1000000 majority.prism majority.props --property change_state -const T=2100
Execution
Walltime:96.88759970664978s
Return code:0
Relative Error:0.0
Log
PRISM
=====

Version: 4.5.dev
Date: Sat Mar 14 14:15:19 UTC 2020
Hostname: e72bdd194fc5
Memory limits: cudd=4g, java(heap)=11g
Command line: prism -javamaxmem 11g -cuddmaxmem 4g -heuristic speed -ddextraactionvars 100 -maxiters 1000000 majority.prism majority.props --property change_state -const T=2100

Parsing model file "majority.prism"...

Type:        CTMC
Modules:     D_def Y_def Z_def CC_def XX_def EE_def 
Variables:   D Y Z CC XX EE 

Parsing properties file "majority.props"...

1 property:
(1) "change_state": P=? [ F<=T ((EE>40)&(CC<20)) ]

---------------------------------------------------------------------

Model checking: "change_state": P=? [ F<=T ((EE>40)&(CC<20)) ]
Property constants: T=2100

Warning: Switching to sparse engine and (backwards) Gauss Seidel (default for heuristic=speed).

Building model...

Computing reachable states...

Reachability (BFS): 44 iterations in 0.04 seconds (average 0.000932, setup 0.00)

Time for model construction: 44.395 seconds.

Type:        CTMC
States:      192000 (1 initial)
Transitions: 1961600

Rate matrix: 9569 nodes (85 terminal), 1961600 minterms, vars: 43r/43c

Computing probabilities...
Engine: Sparse

Number of non-absorbing states: 189000 of 192000 (98.4%)

Building sparse matrix... [n=192000, nnz=1933200, compact] [7.6 MB]
Creating vector for diagonals... [1.5 MB]
Allocating iteration vectors... [3 x 1.5 MB]
TOTAL: [13.4 MB]

Uniformisation: q.t = 3.287227 x 2100.000000 = 6903.175850
Fox-Glynn: left = 6319, right = 7610

Starting iterations...
Iteration 829 (of 7610): max relative diff=0.011121, 5.00 sec so far
Iteration 1656 (of 7610): max relative diff=0.002331, 10.01 sec so far
Iteration 2484 (of 7610): max relative diff=0.000974, 15.02 sec so far
Iteration 3312 (of 7610): max relative diff=0.000551, 20.02 sec so far
Iteration 4139 (of 7610): max relative diff=0.000377, 25.03 sec so far
Iteration 4967 (of 7610): max relative diff=0.000285, 30.03 sec so far
Iteration 5795 (of 7610): max relative diff=0.000229, 35.03 sec so far
Iteration 6612 (of 7610): max relative diff=0.000191, 40.03 sec so far
Iteration 7410 (of 7610): max relative diff=0.000165, 45.03 sec so far

Iterative method: 7610 iterations in 51.03 seconds (average 0.006083, setup 4.74)

Value in the initial state: 0.05429919316250449

Time for model checking: 51.113 seconds.

Result: 0.05429919316250449 (value in the initial state)


Overall running time: 96.133 seconds.

---------------------------------------------------------------------

Note: There was 1 warning during computation.